Nuprl Lemma : nil-iff-no-member
0,22
postcript
pdf
T
:Type,
L
:
T
List.
L
= nil
(
x
:
T
.
(
x
L
))
latex
Definitions
P
Q
,
T
,
True
,
{
T
}
,
P
Q
,
P
&
Q
,
False
,
P
Q
,
P
Q
,
Prop
,
A
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
l
member
wf
,
not
wf
,
nil
member
,
true
wf
,
squash
wf
,
cons
member
origin
T:Type, L:T List. L = nil 
(x:T. 
(x 
L)) T:Type, L:T List. L = nil (x:T. (x L)) 
Q
T Q
Q QA l)x:A. B(x) T